es:ES, A:Type, X, Y:AbsInterface(A).
(e:E. ((e  X))  ((e  Y)))  (e:E. ((e  X))  (X(e) = Y(e)  A))  (X = Y) 

latex

Definitions

f(a), <a, b>, Top, left + right, s = t, x:A. B(x), E, EState(T), Id, , x:AB(x), t  T, pred!(e;e'), SWellFounded(R(x;y)), loc(e), b, A, P  Q, constant_function(f;A;B), Type, kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Unit, Msg(M), type List, IdLnk, EOrderAxioms(E; pred?; info), EqDecider(T), ES, P  Q, t.1, if b then t else f fi , let x,y = A in B(x;y), P  Q, do-apply(f;x), ff, tt, case b of inl(x) => s(x) | inr(y) => t(y), True, , AbsInterface(A), X(e), e  X, x:A.B(x), inr x , False, isl(x), s ~ t, {T}, SQType(T), inl x , can-apply(f;x), outl(x), {x:A| B(x)} , T, SqStable(P)

Lemmas

sq stable from decidable, decidable assert, outl wf, top wf, isl wf, iff wf, assert wf, equal-top, btrue wf, bfalse wf, do-apply wf, val-axiom wf, constant function wf